Nuprl Lemma : wellfounded-anti-reflexive
11,40
postcript
pdf
T
:Type,
R
:(
T
T
). WellFnd{i}(
T
;
x
,
y
.
R
(
x
,
y
))
(
a
:
T
.
R
(
a
,
a
))
latex
Definitions
x
:
A
.
B
(
x
)
,
,
P
Q
,
x
(
s1
,
s2
)
,
x
.
t
(
x
)
,
t
T
,
x
,
y
.
t
(
x
;
y
)
,
A
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
x
(
s
)
,
{
T
}
,
False
Lemmas
not
wf
,
wellfounded
wf
origin
T:Type, R:(T
T
). WellFnd{i}(T;x,y.R(x,y)) 
(a:T. 
R(a,a)) T:Type, R:(TT). WellFnd{i}(T;x,y.R(x,y)) (a:T. R(a,a)) x:A. B(x) Q
x. t(x)
Tx,y. t(x;y)A